module MeteoCal

//Signatures
sig User {
		calendar: one Calendar,
		eventToCreate: set Event,
		eventToUpdate: set Event,
		eventToDelete: set Event,
		id: Int
}


sig Event {
		requests: set Invitation,
		weather: one Weather,
		sends: set Notification,
		tStart: one Date,
		tEnd: one Date
}
{
//Time start must be before Time end
		tStart.year < tEnd.year or 
		tStart.year = tEnd.year and tStart.month < tEnd.month or
		tStart.year = tEnd.year and tStart.month = tEnd.month and tStart.day < tEnd.day or
		tStart.year = tEnd.year and tStart.month = tEnd.month and tStart.day = tEnd.day and tStart.hour < tEnd.hour or
		tStart.year = tEnd.year and tStart.month = tEnd.month and tStart.day = tEnd.day and tStart.hour = tEnd.hour and tStart.minute < tEnd.minute
}

sig Invitation {
		user: one User,
		notification: one Notification
}

sig Calendar{
		events: set Event
}

sig Notification {
		pings: one User, 
		date: one Date
}

sig Email{
		notif: one Notification
}

sig Weather {}


sig Date {
		year: Int,
		month: Int,
		day: Int,
		hour: Int,
		minute: Int
}
/*
{
//Year must be defined between 2000 and 2050
		year >= 2000 and year <= 2050
//Month must be defined between 1 and 12
		month >= 1 and month <= 12
//Day must be defined between 1 and 31
		day >= 1 and day <= 31
//Hour must be defined between 0 and 23
		hour >= 0 and hour <= 23
//Minute must be defined between 0 and 59
		minute >= 0 and minute <= 59
}
*/

//Facts

fact invitationProperties {
//all invitations must have different notifications
	all disj inv1, inv2: Invitation | inv1.notification != inv2.notification
//all invitations must have only one generating event
	all disj e1, e2: Event | e1.requests & e2.requests = none
}

fact userProperties {
//all user must have different calendars
	all disj u1, u2: User | u1.calendar != u2.calendar
//there are no users with the same id
	no disj u1, u2: User | u1.id = u2.id
}

fact calendarProperties {
//there is no calendar without user
	no c: Calendar | no u: User | u.calendar = c
//no user creates event on other user calendar
	all disj u1, u2: User | u1.eventToCreate & u2.eventToCreate = none
//no user updates events that he doesn't own
	all u: User | no e: Event | e in u.eventToUpdate and e !in u.eventToCreate
//no user deletes event that he doesn't own
	all u: User | no e: Event | e in u.eventToDelete and e !in u.eventToCreate
//every event has one and only one tend and tstart
	all e1, e2: Event | (e1.tStart = e2.tStart and e1.tEnd = e2.tEnd) iff e1 = e2
}

fact weatherProperties {
//there is no weather without event
	no w: Weather | no e: Event | e.weather = w
}

fact eventProperties {
//all events must have different weather
	all disj e1, e2: Event | e1.weather != e2.weather

//No events can start before the end of another event (for the same user)
	all u1, u2: User | all disj e1, e2: Event| u1=u2 and e1 = u1.calendar.events and e2 = u1.calendar.events implies 
	e1.tEnd.year < e2.tStart.year or
	e1.tEnd.year = e2.tStart.year and e1.tEnd.month < e2.tStart.month or
	e1.tEnd.year = e2.tStart.year and e1.tEnd.month = e2.tStart.month and e1.tEnd.day < e2.tStart.day or
	e1.tEnd.year = e2.tStart.year and e1.tEnd.month = e2.tStart.month and e1.tEnd.day = e2.tStart.day and e1.tEnd.hour < e2.tStart.hour or
	e1.tEnd.year = e2.tStart.year and e1.tEnd.month = e2.tStart.month and e1.tEnd.day = e2.tStart.day and e1.tEnd.hour = e2.tStart.hour and e1.tEnd.minute < e2.tStart.minute
}

fact emailProperties {
//there is no more than one email for a notification
	all disj m1, m2: Email | m1.notif != m2.notif 
}

//Predicates

pred addEvent(c,c': Calendar, e: Event) {
	not e in c.events
	c'.events=c.events + e
}

run addEvent for 5 but 3 Event

pred deleteEvent(c,c': Calendar, e: Event) {
	e in c.events
	c'.events=c.events - e
}

run deleteEvent for 5 but 3 Event

pred updateEvent(c,c': Calendar, e, e': Event) {
	e in c.events and not e' in c.events
	c'.events=c.events - e + e'
}

run updateEvent for 5 but 3 Event

pred sendInviteToUser(e: Event, i: Invitation, u: User) {
	e in u.calendar.events
	i in e.requests and i.user = u
}

run sendInviteToUser for 1
